\begin{tabbing}
w\_locle($w$;$x$;$y$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$x$ \+
\\[0ex]rel\_star(w{-}E($w$);($\lambda$$x$,$y$. ($\neg$($\uparrow$first($\lambda$$e$.w{-}pred($w$;$e$);$y$)))
\\[0ex]c$\wedge$ ($x$ = pred($\lambda$$e$.w{-}pred($w$;$e$);$y$) $\in$ w{-}E($w$)))) $y$
\-
\end{tabbing}